LevelLiterals.agda:11,19-30
Set (lsuc lzero ⊔ ℓ) != Set
when checking that the expression (A → ⊥) → ⊥ has type Set
